T:Type, X:MaInterface(Top + T), es:ES.
ma-interface-consistent(es;X)
 ([[ma-interface-right(X)]] = es-interface-right([[X]])  AbsInterface(T)) 

latex

Definitions	x:AB(x), P  Q, P  Q, x:A. B(x), Top, left + right, s = t, AbsInterface(A), x:A  B(x), P & Q, P  Q, invert-union(x), ma-interface-right(X), [[X]], es-interface-right(X), <a, b>, ma-interface-consistent(es;X), ES, MaInterface(T), Type
Lemmas	ma-abs-interface-compose